package model.cnf;

import java.io.BufferedWriter;
import java.io.IOException;
import java.util.List;

import controller.xml.XMLBaliseFormat;

/**
 * Represent some statistic on a CNF.
 * 
 * @author GRONOWSKI Stephane svan001@aol.com
 * 
 *         igsat 2010
 * 
 */
public class Stat {

	/** Default value when it is unknown */
	public static final int	UNKNOW_VALUE					= -1;

	private int				numVar							= UNKNOW_VALUE;
	private int				numLiteral						= UNKNOW_VALUE;
	private int				numClause						= UNKNOW_VALUE;
	private int				numUnitClause					= UNKNOW_VALUE;
	private int				numBinaryClause					= UNKNOW_VALUE;

	private double			averageNumOfLiteralPerClause	= UNKNOW_VALUE;


	/**
	 * Export the data in XML
	 * 
	 * @param file
	 *            {@link BufferedWriter} to write
	 * @throws IOException
	 */
	public void exportXML(BufferedWriter file) throws IOException {
		// open
		// file.newLine();
		file.write("<" + XMLBaliseFormat.CNF_STAT + " >");

		// var
		// file.newLine();
		file.write("<" + XMLBaliseFormat.CNF_NUM_VAR + ">");
		file.write(String.valueOf(numVar));
		file.write("</" + XMLBaliseFormat.CNF_NUM_VAR + ">");

		// literal
		// file.newLine();
		file.write("<" + XMLBaliseFormat.CNF_NUM_LITERAL + ">");
		file.write(String.valueOf(numLiteral));
		file.write("</" + XMLBaliseFormat.CNF_NUM_LITERAL + ">");

		// clause
		// file.newLine();
		file.write("<" + XMLBaliseFormat.CNF_NUM_CLAUSE + ">");
		file.write(String.valueOf(numClause));
		file.write("</" + XMLBaliseFormat.CNF_NUM_CLAUSE + ">");

		// unitclause
		// file.newLine();
		file.write("<" + XMLBaliseFormat.CNF_NUM_UNIT_CLAUSE + ">");
		file.write(String.valueOf(numUnitClause));
		file.write("</" + XMLBaliseFormat.CNF_NUM_UNIT_CLAUSE + ">");

		// binaryclause
		// file.newLine();
		file.write("<" + XMLBaliseFormat.CNF_NUM_BINARY_CLAUSE + ">");
		file.write(String.valueOf(numBinaryClause));
		file.write("</" + XMLBaliseFormat.CNF_NUM_BINARY_CLAUSE + ">");

		// average
		// file.newLine();
		file.write("<" + XMLBaliseFormat.CNF_AVERAGE_LIT_CLAUSE + ">");
		file.write(String.valueOf(averageNumOfLiteralPerClause));
		file.write("</" + XMLBaliseFormat.CNF_AVERAGE_LIT_CLAUSE + ">");

		// close
		// file.newLine();
		file.write("</" + XMLBaliseFormat.CNF_STAT + ">");
	}

	/**
	 * Create a new Stat on the CNF.
	 * 
	 * @param cnf_input
	 *            cnf used
	 * @throws IOException
	 *             pb with the CNF file
	 */
	public Stat(MemoryCNF cnf_input) throws IOException {
		computeStat(cnf_input);
	}

	/**
	 * Create a new Stat on the CNF.
	 * 
	 * @param cnf_input
	 *            cnf used
	 * @throws IOException
	 *             pb with the CNF file
	 */
	public Stat(FileCNF cnf_input) throws IOException {
		computeStat(cnf_input);
	}

	/**
	 * Create a new Stat instance.
	 */
	public Stat() {
	}

	/**
	 * Compute the statistics of a {@link MemoryCNF}.
	 * 
	 * @param cnf
	 *            the cnf.
	 * @throws IOException
	 *             problem with the file.
	 */
	public void computeStat(MemoryCNF cnf) throws IOException {
		List<Clause> my_clause = cnf.getClauses();
		numLiteral = numUnitClause = numBinaryClause = 0;

		numClause = my_clause.size();
		for (int i = 0 ; i < numClause ; i++)
		{
			Clause cl = my_clause.get(i);
			if (cl.isUnit())
				numUnitClause++;
			if (cl.isBinary())
				numBinaryClause++;
			numLiteral += cl.size();
		}
		averageNumOfLiteralPerClause = (double) numLiteral / numClause;
		averageNumOfLiteralPerClause = Math.round(averageNumOfLiteralPerClause * 1000.0) / 1000.0;
		numVar = cnf.getDeclaredNumVar();
	}

	/**
	 * Compute the statistics of a {@link FileCNF}.
	 * 
	 * @param cnf
	 *            the cnf.
	 * @throws IOException
	 *             problem with the file.
	 */
	public void computeStat(FileCNF cnf) throws IOException {
		numLiteral = numUnitClause = numBinaryClause = 0;

		cnf.check();
		numClause = cnf.getDeclaredNumClause();
		numVar = cnf.getDeclaredNumVar();

		for (int i = 0 ; i < numClause ; i++)
		{
			Clause cl = cnf.getNextClause();
			if (cl.isUnit())
				numUnitClause++;
			if (cl.isBinary())
				numBinaryClause++;
			numLiteral += cl.size();
		}

		averageNumOfLiteralPerClause = (double) numLiteral / numClause;
		averageNumOfLiteralPerClause = Math.round(averageNumOfLiteralPerClause * 1000.0) / 1000.0;

	}

	@Override
	public String toString() {
		return "#Variables : " + numVar + "\n#Clauses : " + numClause + "\n#Literals : " + numLiteral + "\n#Unit clauses : "
				+ numUnitClause + "\n#Binary clauses : " + numBinaryClause + "\nAverage lit/clause : " + averageNumOfLiteralPerClause;
	}

	/**
	 * 
	 * @return the number of var.
	 */
	public int getNumVar() {
		return numVar;
	}

	/**
	 * 
	 * @return the number of literal.
	 */
	public int getNumLiteral() {
		return numLiteral;
	}

	/**
	 * 
	 * @return the number of clause.
	 */
	public int getNumClause() {
		return numClause;
	}

	/**
	 * 
	 * @return the number of unit clause.
	 */
	public int getNumUnitClause() {
		return numUnitClause;
	}

	/**
	 * 
	 * @return the number of binary clause.
	 */
	public int getNumBinaryClause() {
		return numBinaryClause;
	}

	/**
	 * @return the averageNumOfLiteralPerClause
	 */
	public double getAverageNumOfLiteralPerClause() {
		return averageNumOfLiteralPerClause;
	}

	/**
	 * Set the number of variable.
	 * 
	 * @param numVar
	 *            new number.
	 */
	public void setNumVar(int numVar) {
		if (numVar == UNKNOW_VALUE || numVar >= 0)
			this.numVar = numVar;
	}

	/**
	 * Set the number of literal.
	 * 
	 * @param numLiteral
	 *            new number.
	 */
	public void setNumLiteral(int numLiteral) {
		if (numLiteral == UNKNOW_VALUE || numLiteral >= 0)
		{
			this.numLiteral = numLiteral;
			if (numLiteral != UNKNOW_VALUE && numClause != UNKNOW_VALUE)
			{
				averageNumOfLiteralPerClause = (double) numLiteral / numClause;
				averageNumOfLiteralPerClause = Math.round(averageNumOfLiteralPerClause * 1000.0) / 1000.0;
			}
		}
	}

	/**
	 * Set the number of clause.
	 * 
	 * @param numClause
	 *            new number.
	 */
	public void setNumClause(int numClause) {
		if (numClause == UNKNOW_VALUE || numClause >= 0)
		{
			this.numClause = numClause;
			if (numLiteral != UNKNOW_VALUE && numClause != UNKNOW_VALUE)
			{
				averageNumOfLiteralPerClause = (double) numLiteral / numClause;
				averageNumOfLiteralPerClause = Math.round(averageNumOfLiteralPerClause * 1000.0) / 1000.0;
			}
		}

	}

	/**
	 * Set the number of unit clause.
	 * 
	 * @param numUnitClause
	 *            new value.
	 */
	public void setNumUnitClause(int numUnitClause) {
		this.numUnitClause = numUnitClause;
	}

	/**
	 * Set the number of binary clause.
	 * 
	 * @param numBinaryClause
	 *            new value.
	 */
	public void setNumBinaryClause(int numBinaryClause) {
		this.numBinaryClause = numBinaryClause;
	}


	/**
	 * Set the average of literal per clause (use it only for import of {@link Stat}.
	 * 
	 * @param averageNumOfLiteralPerClause
	 *            the averageNumOfLiteralPerClause to set
	 */
	public void setAverageNumOfLiteralPerClause(double averageNumOfLiteralPerClause) {
		this.averageNumOfLiteralPerClause = averageNumOfLiteralPerClause;
	}

	/**
	 * Add clause to the compute stat.
	 * 
	 * @param clause
	 *            new clause.
	 * @param nbVar
	 *            number of var in the clause.
	 */
	public void addClause(Clause clause, int nbVar) {
		numClause++;
		if (clause.isUnit())
			numUnitClause++;
		if (clause.isBinary())
			numBinaryClause++;
		numLiteral += clause.size();

		averageNumOfLiteralPerClause = (double) numLiteral / numClause;
		averageNumOfLiteralPerClause = Math.round(averageNumOfLiteralPerClause * 1000.0) / 1000.0;
		numVar += nbVar;
	}

	@Override
	public boolean equals(Object o) {
		if (!(o instanceof Stat))
			return false;
		Stat s = (Stat) o;
		if (numVar != s.getNumVar())
			return false;
		if (numLiteral != s.getNumLiteral())
			return false;
		if (numClause != s.getNumClause())
			return false;
		if (numUnitClause != s.getNumUnitClause())
			return false;
		if (numBinaryClause != s.getNumBinaryClause())
			return false;
		return true;
	}
}
